update-spec-decl(upd; ds) == z:Id. (z  update-spec-vars(upd))  (fpf-dom(id-deq; z; ds)) 

latex

---

clarification:

update-spec-decl(upd; ds)
== z:Id. (z  update-spec-vars(upd)  Id)  (fpf-dom(id-deq; z; ds)) 

latex

Definitions	x:A. B(x), P  Q, (x  l), update-spec-vars(upd), Id, b, fpf-dom(eq; x; f), id-deq
FDL editor aliases	update-spec-decl